ePMC

Benchmark
Model:consensus v.1 (MDP)
Parameter(s)N = 6, K = 2
Property:disagree (prob-reach)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ../epmc-standard.jar check --model-input-files consensus.6.prism --model-input-type prism --property-input-files consensus.props --property-input-names disagree --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const K=2
Execution
Walltime:139.3075611591339s
Return code:0
Relative Error:3.08059305525717e-05
Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property disagree
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 18086 18086
build-model-states-explored 43690 25604
build-model-states-explored 77106 33415
build-model-states-explored 105468 28363
build-model-states-explored 147435 41966
build-model-states-explored 191396 43961
build-model-states-explored 214807 23412
build-model-states-explored 259875 45067
build-model-states-explored 303376 43502
build-model-states-explored 347724 44348
build-model-states-explored 391766 44041
build-model-states-explored 436461 44695
build-model-states-explored 442401 5941
build-model-states-explored 478856 36455
build-model-states-explored 524396 45540
build-model-states-explored 569918 45522
build-model-states-explored 612723 42804
build-model-states-explored 657565 44843
build-model-states-explored 702386 44820
build-model-states-explored 751720 49335
build-model-states-explored 807548 55828
build-model-states-explored 865872 58324
build-model-states-explored 921836 55964
build-model-states-explored 979361 57525
build-model-states-explored 1000069 20708
build-model-states-explored 1000069 0
build-model-states-explored 1035594 35525
build-model-states-explored 1089353 53759
build-model-states-explored 1145022 55668
build-model-states-explored 1201481 56459
build-model-states-explored 1257493 56013
build-model-done 1258240 31
iterating
iterating-progress-unbounded 34 3.0 1
iterating-progress-unbounded 72 5.5 2
iterating-progress-unbounded 111 5.9512820512820515 3
iterating-progress-unbounded 150 0.5460180064044169 4
iterating-progress-unbounded 189 0.2318498015787259 5
iterating-progress-unbounded 227 0.1379980961240851 6
iterating-progress-unbounded 266 0.09369625724007055 7
iterating-progress-unbounded 305 0.06779232040198518 8
iterating-progress-unbounded 344 0.051331237917146826 9
iterating-progress-unbounded 383 0.040361967998447976 10
iterating-progress-unbounded 422 0.032525414055766186 11
iterating-progress-unbounded 461 0.026945410554817868 12
iterating-progress-unbounded 499 0.022428453008366794 13
iterating-progress-unbounded 538 0.018904566679837618 14
iterating-progress-unbounded 577 0.016088687523976932 15
iterating-progress-unbounded 616 0.013916633269840918 16
iterating-progress-unbounded 655 0.01198425532708601 17
iterating-progress-unbounded 694 0.010402672400272114 18
iterating-progress-unbounded 732 0.009098920247824596 19
iterating-progress-unbounded 771 0.00803068041989846 20
iterating-progress-unbounded 810 0.007041091951254402 21
iterating-progress-unbounded 849 0.006203435624201056 22
iterating-progress-unbounded 888 0.005481346109440134 23
iterating-progress-unbounded 927 0.004852711609755952 24
iterating-progress-unbounded 965 0.004334821906856982 25
iterating-progress-unbounded 1004 0.003848704470690533 26
iterating-progress-unbounded 1043 0.003422872519456593 27
iterating-progress-unbounded 1082 0.0030469203362877006 28
iterating-progress-unbounded 1121 0.00273382317550121 29
iterating-progress-unbounded 1160 0.0024326632588841574 30
iterating-progress-unbounded 1199 0.0021695021841482433 31
iterating-progress-unbounded 1237 0.00194017165675711 32
iterating-progress-unbounded 1276 0.0017443433015296485 33
iterating-progress-unbounded 1315 0.001554823903327216 34
iterating-progress-unbounded 1354 0.001388383313154648 35
iterating-progress-unbounded 1393 0.0012404235935170814 36
iterating-progress-unbounded 1432 0.0011081347934694449 37
iterating-progress-unbounded 1470 9.969481350470485E-4 38
iterating-progress-unbounded 1509 8.903646486886319E-4 39
iterating-progress-unbounded 1548 7.954449375562665E-4 40
iterating-progress-unbounded 1587 7.104580841181802E-4 41
iterating-progress-unbounded 1626 6.389783358661024E-4 42
iterating-progress-unbounded 1665 5.694858074900395E-4 43
iterating-progress-unbounded 1703 5.092794570638948E-4 44
iterating-progress-unbounded 1742 4.545533336367851E-4 45
iterating-progress-unbounded 1781 4.0853708130294164E-4 46
iterating-progress-unbounded 1820 3.6380051630441725E-4 47
iterating-progress-unbounded 1859 3.243983596775024E-4 48
iterating-progress-unbounded 1898 2.8931275934612066E-4 49
iterating-progress-unbounded 1937 2.5791418827372125E-4 50
iterating-progress-unbounded 1975 2.3154103693366195E-4 51
iterating-progress-unbounded 2014 2.0625152983913067E-4 52
iterating-progress-unbounded 2053 1.8375293299301596E-4 53
iterating-progress-unbounded 2092 1.6363777466503265E-4 54
iterating-progress-unbounded 2131 1.4676119680538097E-4 55
iterating-progress-unbounded 2170 1.3038132804083757E-4 56
iterating-progress-unbounded 2209 1.1598512078278203E-4 57
iterating-progress-unbounded 2247 1.0339059262919422E-4 58
iterating-progress-unbounded 2286 9.263714957521773E-5 59
iterating-progress-unbounded 2325 8.221075052185507E-5 60
iterating-progress-unbounded 2364 7.305742419577066E-5 61
iterating-progress-unbounded 2403 6.493489997715419E-5 62
iterating-progress-unbounded 2442 5.76912321670974E-5 63
iterating-progress-unbounded 2481 5.163046546775073E-5 64
iterating-progress-unbounded 2519 4.58368046659166E-5 65
iterating-progress-unbounded 2558 4.070140564790617E-5 66
iterating-progress-unbounded 2597 3.612672422254734E-5 67
iterating-progress-unbounded 2636 3.2303507203062216E-5 68
iterating-progress-unbounded 2675 2.860501628866883E-5 69
iterating-progress-unbounded 2714 2.536614345638743E-5 70
iterating-progress-unbounded 2753 2.249910148729207E-5 71
iterating-progress-unbounded 2791 2.0140816589339066E-5 72
iterating-progress-unbounded 2830 1.781960123940843E-5 73
iterating-progress-unbounded 2869 1.5788861149058768E-5 74
iterating-progress-unbounded 2908 1.3993013094131371E-5 75
iterating-progress-unbounded 2947 1.2396848502664433E-5 76
iterating-progress-unbounded 2986 1.1065959497791434E-5 77
iterating-progress-unbounded 3024 9.79743864434923E-6 78
iterating-progress-unbounded 3063 8.676653269942227E-6 79
iterating-progress-unbounded 3102 7.68135797760608E-6 80
iterating-progress-unbounded 3141 6.852212169727311E-6 81
iterating-progress-unbounded 3179 6.062519338676108E-6 82
iterating-progress-unbounded 3218 5.365369302537708E-6 83
iterating-progress-unbounded 3257 4.746769203215244E-6 84
iterating-progress-unbounded 3295 4.2318513284422415E-6 85
iterating-progress-unbounded 3334 3.7417734271424038E-6 86
iterating-progress-unbounded 3373 3.3094508656437177E-6 87
iterating-progress-unbounded 3412 2.926117656751128E-6 88
iterating-progress-unbounded 3450 2.607268769669259E-6 89
iterating-progress-unbounded 3489 2.3039926474364075E-6 90
iterating-progress-unbounded 3528 2.03663994624688E-6 91
iterating-progress-unbounded 3567 1.7997395242914254E-6 92
iterating-progress-unbounded 3606 1.6028225153431076E-6 93
iterating-progress-unbounded 3644 1.4156307914353157E-6 94
iterating-progress-unbounded 3683 1.2507148495726512E-6 95
iterating-progress-unbounded 3722 1.1046715100519818E-6 96
iterating-progress-unbounded 3761 9.833511774632406E-7 97
iterating-progress-unbounded 3800 8.666024620918766E-7 98
iterating-progress-unbounded 3839 7.649283708456305E-7 99
iterating-progress-unbounded 3877 6.767607268549477E-7 100
iterating-progress-unbounded 3916 6.021800817455539E-7 101
iterating-progress-unbounded 3955 5.304450202727469E-7 102
iterating-done 3974 102
model-checking-done 138
command-check-result-is 0.3636335471480052 disagree